`timescale 1ns/1ps
// 计数器属性模块（通过 bind 绑定到 DUT）
module _props (
    input logic       clk,
    input logic       rst_n,
    input logic       en,
    input logic [3:0] cnt,
    input logic       ovf
);

// 手动实现$past功能
reg [3:0] past_cnt;
always @(posedge clk) past_cnt <= cnt;

// 复位后计数器为0且无溢出
property p_reset;
    !rst_n |=> cnt == 0 && ovf == 0;
endproperty
a_reset: assert property (@(posedge clk)p_reset);

// 使能时计数器递增（除非达到15）
property p_increment;
    en && cnt < 4'hF |=> cnt == $past(cnt) + 1;
endproperty
a_increment: assert property (@(posedge clk)p_increment);

// 溢出条件
property p_overflow;
    en && cnt == 4'hF |=> cnt == 0 && ovf;
endproperty
a_overflow: assert property (@(posedge clk)p_overflow);

// ------------------------------
// 覆盖点
// ------------------------------
genvar i;
generate
    for (i=0; i<16; i++) begin : gen_covers
        // 每个值对应的覆盖属性
        cover property (
            @(posedge clk) 
            cnt == i
        ) $display("Covered cnt=%0d at %0t", i, $time);
    end
endgenerate

endmodule